<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Formula</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Formula";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/DjVars.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Hyp.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Formula.html" target="_top">Frames</a></li>
<li><a href="Formula.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class Formula" class="title">Class Formula</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.Formula</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/lang/LogicFormula.html" title="class in mmj.lang">LogicFormula</a>, <a href="../../mmj/lang/VarHypFormula.html" title="class in mmj.lang">VarHypFormula</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">Formula</span>
extends java.lang.Object</pre>
<div class="block">Formula is, basically just an array of Sym, with a counter.
 <p>
 Sub-Classes of Formula exist: VarHypFormula and LogicFormula but their
 function is basically just to simplify certain coding in VarHyp, LogHyp, etc.
 In theory, the distinction would be useful for creating default exprRPN's.
 <p>
 Formula: contains Cnst in sym[0], followed by the formula's "expression",
 which consists of zero or more Cnst's and Var's in sym[1]...sym[cnt - 1].
 <p>
 Formula Factoids:
 <ul>
 <li>A formula must have length >= 1.
 <li>sym[0], the first Sym in a Formula must be a Cnst.
 <li>sym[0] is the Type Code of the Formula, and by extension, the Stmt's Type
 Code.
 <li>sym[1] through sym[sym.length - 1] are referred to in mmj as the
 Formula's "Expression" -- which is simply the Formula minus its Type Code.
 <li>Every Stmt has a Formula, but a Formula can be created without a
 corresponding Stmt (which is the reason Formula was made into a class.)</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier</th>
<th class="colLast" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>&nbsp;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#Formula(java.util.Collection)">Formula</a></strong>(java.util.Collection&lt;<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symList)</code>
<div class="block">Construct using Sym List.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>&nbsp;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#Formula(int, mmj.lang.Sym[])">Formula</a></strong>(int&nbsp;workCnt,
       <a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;workFormula)</code>
<div class="block">Construct using cnt and Sym array.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected </code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#Formula(java.util.Map, int, java.lang.String)">Formula</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       int&nbsp;sz,
       java.lang.String&nbsp;typS)</code>
<div class="block">Construct Formula of given size and Type.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static &lt;T extends <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;<br>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#accumHypInList(java.util.List, T)">accumHypInList</a></strong>(java.util.List&lt;T&gt;&nbsp;hypList,
              T&nbsp;hypNew)</code>
<div class="block">Accumulate unique hypotheses (no duplicates), storing them in an array
 list in order of their appearance in the database.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#buildMandVarHypArray(mmj.lang.Hyp[])">buildMandVarHypArray</a></strong>(<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;tempHypArray)</code>
<div class="block">Uses an array of Hyps to build an array of VarHyps containing only the
 VarHyps needed for the variables actually used in the Formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#buildRuleFormatExpr(mmj.lang.VarHyp[])">buildRuleFormatExpr</a></strong>(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</code>
<div class="block">Builds a "rule format" version of the Formula's Expression.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#computeWidthOfWidestExprCnst()">computeWidthOfWidestExprCnst</a></strong>()</code>
<div class="block">Computes the width in characters of the widest Cnst in the Formula's
 Expression.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#constructTempDummyFormula(mmj.lang.Cnst, java.lang.String)">constructTempDummyFormula</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ,
                         java.lang.String&nbsp;dummySym)</code>
<div class="block">Construct a temporary dummy Formula for transient use.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#equals(java.lang.Object)">equals</a></strong>(java.lang.Object&nbsp;obj)</code>
<div class="block">Compare for equality with another Formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#exprEquals(java.lang.Object)">exprEquals</a></strong>(java.lang.Object&nbsp;obj)</code>
<div class="block">Compare Expression for equality with another Formula's expr (don't
 compare Type Codes, in other words).</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#exprToString()">exprToString</a></strong>()</code>
<div class="block">Computes a character string version of the expression portion of the
 formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getCnt()">getCnt</a></strong>()</code>
<div class="block">Return Formula's length.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getExpr()">getExpr</a></strong>()</code>
<div class="block">Return Formula's Expression (sym[1]...sym[cnt - 1]).</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getParseNodeHolderExpr(mmj.lang.Hyp[])">getParseNodeHolderExpr</a></strong>(<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;hypArray)</code>
<div class="block">Builds a "custom" version of an Expression in which an array of
 ParseNodeHolders is output for use in generating a ParseTree.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getParseNodeHolderExpr(mmj.lang.VarHyp[])">getParseNodeHolderExpr</a></strong>(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</code>
<div class="block">Builds a "custom" version of an Expression in which an array of
 ParseNodeHolders is output for use in generating a ParseTree.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getSym()">getSym</a></strong>()</code>
<div class="block">Return Formula's symbol array.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#getTyp()">getTyp</a></strong>()</code>
<div class="block">Return Formula Type Code.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#hashCode()">hashCode</a></strong>()</code>
<div class="block">Computes hashcode for this Formula.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#setTyp(mmj.lang.Cnst)">setTyp</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</code>
<div class="block">Set Formula Type Code.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#setTyp(java.util.Map, java.lang.String)">setTyp</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
      java.lang.String&nbsp;typS)</code>
<div class="block">Set Formula Type Code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#srcStmtEquals(mmj.mmio.SrcStmt)">srcStmtEquals</a></strong>(<a href="../../mmj/mmio/SrcStmt.html" title="class in mmj.mmio">SrcStmt</a>&nbsp;srcStmt)</code>
<div class="block">Compare SrcStmt typ and symList to Formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#toProofWorksheetStringBuilder(java.lang.StringBuilder, int, int)">toProofWorksheetStringBuilder</a></strong>(java.lang.StringBuilder&nbsp;sb,
                             int&nbsp;leftColContinuation,
                             int&nbsp;marginRight)</code>
<div class="block">Formats formula symbol strings into a column of characters within a text
 area.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#toString()">toString</a></strong>()</code>
<div class="block">Computes a character string version of Formula for printing.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.StringBuilder</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Formula.html#toStringBuilderLineList(java.util.List, java.lang.StringBuilder, int, int, java.lang.String)">toStringBuilderLineList</a></strong>(java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;list,
                       java.lang.StringBuilder&nbsp;sb,
                       int&nbsp;leftColContinuation,
                       int&nbsp;marginRight,
                       java.lang.String&nbsp;endToken)</code>
<div class="block">Formats formula into StringBuilder lines in a List.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Formula(int, mmj.lang.Sym[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Formula</h4>
<pre>public&nbsp;Formula(int&nbsp;workCnt,
       <a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;workFormula)</pre>
<div class="block">Construct using cnt and Sym array.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workCnt</code> - the correct length of the formula.</dd><dd><code>workFormula</code> - the formula's Sym array.</dd></dl>
</li>
</ul>
<a name="Formula(java.util.Collection)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Formula</h4>
<pre>public&nbsp;Formula(java.util.Collection&lt;<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symList)</pre>
<div class="block">Construct using Sym List. Enforces rule that first symbol must be a Cnst,
 just in case.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symList</code> - List containing formula symbols</dd></dl>
</li>
</ul>
<a name="Formula(java.util.Map, int, java.lang.String)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Formula</h4>
<pre>protected&nbsp;Formula(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       int&nbsp;sz,
       java.lang.String&nbsp;typS)
           throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct Formula of given size and Type.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>sz</code> - Size of the formula</dd><dd><code>typS</code> - Formula Type code</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="constructTempDummyFormula(mmj.lang.Cnst, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>constructTempDummyFormula</h4>
<pre>public static&nbsp;<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;constructTempDummyFormula(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ,
                                java.lang.String&nbsp;dummySym)</pre>
<div class="block">Construct a temporary dummy Formula for transient use. This is useful in
 ProofWorksheet.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - is the Formula's TypCd Cnst.</dd><dd><code>dummySym</code> - a string of characters that should not have non-printable
            characters or whitespace (else renderFormula may come out
            wrong!)</dd>
<dt><span class="strong">Returns:</span></dt><dd>the dummy Formula</dd></dl>
</li>
</ul>
<a name="getTyp()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;getTyp()</pre>
<div class="block">Return Formula Type Code.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Formula Type Code (which is sym[0]).</dd></dl>
</li>
</ul>
<a name="setTyp(mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setTyp</h4>
<pre>public&nbsp;void&nbsp;setTyp(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</pre>
<div class="block">Set Formula Type Code.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - Formula Type Code (sym[0]).</dd></dl>
</li>
</ul>
<a name="getExpr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getExpr</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;getExpr()</pre>
<div class="block">Return Formula's Expression (sym[1]...sym[cnt - 1]).</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Formula's Expression (sym[1]...sym[cnt - 1]).</dd></dl>
</li>
</ul>
<a name="getCnt()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCnt</h4>
<pre>public&nbsp;int&nbsp;getCnt()</pre>
<div class="block">Return Formula's length.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Formula's length.</dd></dl>
</li>
</ul>
<a name="getSym()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSym</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>[]&nbsp;getSym()</pre>
<div class="block">Return Formula's symbol array.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Formula's symbol array.</dd></dl>
</li>
</ul>
<a name="setTyp(java.util.Map, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setTyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&nbsp;setTyp(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
         java.lang.String&nbsp;typS)
           throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Set Formula Type Code.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Symbol Table (Map).</dd><dd><code>typS</code> - Type Code String identifying a Cnst.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Type Code symbol.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if Type Code is undefined or not defined as a Cnst.</dd></dl>
</li>
</ul>
<a name="getParseNodeHolderExpr(mmj.lang.VarHyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getParseNodeHolderExpr</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;getParseNodeHolderExpr(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</pre>
<div class="block">Builds a "custom" version of an Expression in which an array of
 ParseNodeHolders is output for use in generating a ParseTree.
 <p>
 The key fact about the output ParseNodeHolders is that a Cnst in the
 Formula Expression just goes into the holder's "mObj" -- it will not be
 part of the ParseTree and the ParseNode element is null.
 <p>
 On the other hand, Variables in the Formula's Expression are converted
 into ParseNodes with Stmt = the VarHyp; the ParseNodeHolder's "mObj"
 element is set to the VarHyp Stmt reference -- and this ParseNode will be
 part of the ultimate Parse Tree. In effect, we're "parsing" VarHyps and
 creating their output ParseNodes at this time.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>varHypArray</code> - Array of VarHyp for Formula.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ParseNodeHolder array.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if unable to find a VarHyp for one of
             the Formula's Var's.</dd></dl>
</li>
</ul>
<a name="getParseNodeHolderExpr(mmj.lang.Hyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getParseNodeHolderExpr</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;getParseNodeHolderExpr(<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;hypArray)</pre>
<div class="block">Builds a "custom" version of an Expression in which an array of
 ParseNodeHolders is output for use in generating a ParseTree.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>hypArray</code> - Array of Hyp for Formula.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ParseNodeHolder array.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if unable to find a VarHyp for one of
             the Formula's Var's.</dd></dl>
</li>
</ul>
<a name="buildRuleFormatExpr(mmj.lang.VarHyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildRuleFormatExpr</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;buildRuleFormatExpr(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</pre>
<div class="block">Builds a "rule format" version of the Formula's Expression. Each Cnst in
 the Expression is output unchanged, while the Type Code (a Cnst) of each
 Var is output instead of the var -- this requires looking up the Var's
 VarHyp in the input varHypArray. For example, Expression "( ph -> ps )"
 is output as "( wff -> wff )".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>varHypArray</code> - Array of VarHyp for Formula.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ruleFormatExpr in an array of Cnst.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if unable to find a VarHyp for one of
             the Formula's Var's.</dd></dl>
</li>
</ul>
<a name="buildMandVarHypArray(mmj.lang.Hyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildMandVarHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;buildMandVarHypArray(<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;tempHypArray)</pre>
<div class="block">Uses an array of Hyps to build an array of VarHyps containing only the
 VarHyps needed for the variables actually used in the Formula.
 <p>
 Note: if the input array of Hyps does not contain all of the necessary
 VarHyps, an IllegalArgumentException is thrown! No mercy.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>tempHypArray</code> - array of Hyp.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ruleFormatExpr in an array of Cnst.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if unable to find a VarHyp for one of
             the Formula's Var's.</dd></dl>
</li>
</ul>
<a name="hashCode()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hashCode</h4>
<pre>public&nbsp;int&nbsp;hashCode()</pre>
<div class="block">Computes hashcode for this Formula.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>hashCode</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
<dt><span class="strong">Returns:</span></dt><dd>hashcode for the Formula</dd></dl>
</li>
</ul>
<a name="exprEquals(java.lang.Object)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exprEquals</h4>
<pre>public&nbsp;boolean&nbsp;exprEquals(java.lang.Object&nbsp;obj)</pre>
<div class="block">Compare Expression for equality with another Formula's expr (don't
 compare Type Codes, in other words).
 <p>
 Equal if and only if the Sym strings are equal. and the obj to be
 compared to this object is not null and is a Formula as well.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>obj</code> - Formula whose Expression will be compared to this Formula's
            Expression.</dd>
<dt><span class="strong">Returns:</span></dt><dd>returns true if equal, otherwise false.</dd></dl>
</li>
</ul>
<a name="srcStmtEquals(mmj.mmio.SrcStmt)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>srcStmtEquals</h4>
<pre>public&nbsp;boolean&nbsp;srcStmtEquals(<a href="../../mmj/mmio/SrcStmt.html" title="class in mmj.mmio">SrcStmt</a>&nbsp;srcStmt)</pre>
<div class="block">Compare SrcStmt typ and symList to Formula.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>srcStmt</code> - from mmj.mmio.Statementizer.java.</dd>
<dt><span class="strong">Returns:</span></dt><dd>returns true if label and symList are identical to the Formula
         otherwise false.</dd></dl>
</li>
</ul>
<a name="equals(java.lang.Object)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>equals</h4>
<pre>public&nbsp;boolean&nbsp;equals(java.lang.Object&nbsp;obj)</pre>
<div class="block">Compare for equality with another Formula.
 <p>
 Equal if and only if the Sym strings are equal. and the obj to be
 compared to this object is not null and is a Formula as well.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>equals</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>obj</code> - Formula that will be compared to this Formula.</dd>
<dt><span class="strong">Returns:</span></dt><dd>returns true if equal, otherwise false.</dd></dl>
</li>
</ul>
<a name="toString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toString</h4>
<pre>public&nbsp;java.lang.String&nbsp;toString()</pre>
<div class="block">Computes a character string version of Formula for printing.
 <p>
 Note: LogicalSystem does not validate for "printable" characters in Sym,
 and output of certain non-printable characters can cause abrupt
 termination of DOS windows (though mmj.mmio does extensive validation,
 LogicalSystem itself is unconcerned about the contents of Sym id
 strings.)</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>toString</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
<dt><span class="strong">Returns:</span></dt><dd>String for the Formula</dd></dl>
</li>
</ul>
<a name="exprToString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exprToString</h4>
<pre>public&nbsp;java.lang.String&nbsp;exprToString()</pre>
<div class="block">Computes a character string version of the expression portion of the
 formula.
 <p>
 Note: the "expression" here is the 2nd thru nth symbols of the formula --
 that is, the type code at the start is discarded.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>String for the expression portion of Formula</dd></dl>
</li>
</ul>
<a name="toProofWorksheetStringBuilder(java.lang.StringBuilder, int, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toProofWorksheetStringBuilder</h4>
<pre>public&nbsp;int&nbsp;toProofWorksheetStringBuilder(java.lang.StringBuilder&nbsp;sb,
                                int&nbsp;leftColContinuation,
                                int&nbsp;marginRight)</pre>
<div class="block">Formats formula symbol strings into a column of characters within a text
 area. Weird because it does not indent on the first line, but the output
 can be simply "append"ed to the text area, which presumably already has
 data to the left of "leftColContinuation" on line 1. the first line of
 text -- to</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>sb</code> - StringBuilder to append to.</dd><dd><code>leftColContinuation</code> - the leftmost column in the text area for use
            by formulas.</dd><dd><code>marginRight</code> - the rightmost column for use by formulas.</dd>
<dt><span class="strong">Returns:</span></dt><dd>nbrLines used by the output formula.</dd></dl>
</li>
</ul>
<a name="toStringBuilderLineList(java.util.List, java.lang.StringBuilder, int, int, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toStringBuilderLineList</h4>
<pre>public&nbsp;java.lang.StringBuilder&nbsp;toStringBuilderLineList(java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;list,
                                              java.lang.StringBuilder&nbsp;sb,
                                              int&nbsp;leftColContinuation,
                                              int&nbsp;marginRight,
                                              java.lang.String&nbsp;endToken)</pre>
<div class="block">Formats formula into StringBuilder lines in a List.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>list</code> - list of StringBuilder lines.</dd><dd><code>sb</code> - StringBuilder to append to.</dd><dd><code>leftColContinuation</code> - the leftmost column in the text area for use
            by formulas.</dd><dd><code>marginRight</code> - the rightmost column for use by formulas.</dd><dd><code>endToken</code> - string such as "$." or "$="</dd>
<dt><span class="strong">Returns:</span></dt><dd>final StringBuilder line in use.</dd></dl>
</li>
</ul>
<a name="accumHypInList(java.util.List,mmj.lang.Hyp)">
<!--   -->
</a><a name="accumHypInList(java.util.List, T)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumHypInList</h4>
<pre>public static&nbsp;&lt;T extends <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;void&nbsp;accumHypInList(java.util.List&lt;T&gt;&nbsp;hypList,
                                  T&nbsp;hypNew)</pre>
<div class="block">Accumulate unique hypotheses (no duplicates), storing them in an array
 list in order of their appearance in the database.</div>
<dl><dt><span class="strong">Type Parameters:</span></dt><dd><code>T</code> - the actual type of the list</dd><dt><span class="strong">Parameters:</span></dt><dd><code>hypList</code> - -- List of Hyp's. Is updated with unique variable
            hypotheses in the expression. Because the list is maintained
            in database statement sequence order, hypList should either be
            empty (new) before the call, or already be in that order (see
            <code>accumHypInList</code>.</dd><dd><code>hypNew</code> - candidate Hyp to be added to hypList if not already there.</dd></dl>
</li>
</ul>
<a name="computeWidthOfWidestExprCnst()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>computeWidthOfWidestExprCnst</h4>
<pre>public&nbsp;int&nbsp;computeWidthOfWidestExprCnst()</pre>
<div class="block">Computes the width in characters of the widest Cnst in the Formula's
 Expression.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>width in characters of the widest Cnst in the Formula's
         Expression -- or -1 if the Expression is null or if it contains
         no constants.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/DjVars.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Hyp.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Formula.html" target="_top">Frames</a></li>
<li><a href="Formula.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
